$\forall$${\it es}$:ES, $A$, $B$:Type, ${\it Ia}$:AbsInterface($A$), $f$:($A$$\rightarrow$$B$), $Q$:(E$\rightarrow$E$\rightarrow\mathbb{P}$).
\\[0ex]Q{-}R{-}glued(${\it es}$; $B$; ($\lambda$$e$.$f$(${\it Ia}$($e$))); ${\it Ia}$; $Q$; $f$'${\it Ia}$; $Q$)